es:ES, i:Id, ds:x:Id fp Type, P:(State(ds)),
init:{f:x:Id fp ds(x)?Top| x:Id. (x  dom(ds))  (x  dom(f))} .
pre-init-p(es; i; ds; init; P)   

latex

Definitions	Top, ff, tt, if b then t else f fi , f(x)?z, State(ds), x. t(x), x:A. B(x), pre-init-p(es; i; ds; init; P), , t  T, P  Q, x:A. B(x), False, A, P & Q, P  Q, Unit, , x(s),
Lemmas	fpf-ap wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, event system wf, bool wf, decl-state wf, fpf-trivial-subtype-top, fpf-dom wf, top wf, id-deq wf, fpf-cap wf, fpf wf, es-loc wf, Id wf, es-E wf, assert wf